Corelab Seminar
2016-2017
Antonis Achilleos
Determinizing Monitors for HML with Recursion
Abstract.
In this talk, we will examine the determinization of monitors for Hennessy-Milner with recursion. We demonstrate that every monitor is equivalent to a deterministic one, which is at most doubly exponential in size with respect to the original monitor. When monitors are described as CCS-like processes, this doubly exponential bound is optimal. When (deterministic) monitors are described as finite automata (as their LTS), then they can be exponentially more succinct than their CCS process form.
The talk is based on joint work with Luca Aceto, Adrian Francalanza, Anna Ingólfsdóttir and Sævar Örn Kjartansson, which is available at: https://arxiv.org/abs/1611.10212